f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
↳ QTRS
↳ DependencyPairsProof
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
F(.(.(x, y), z)) → F(.(x, .(y, z)))
G(.(x, .(y, z))) → G(.(.(x, y), z))
F(.(nil, y)) → F(y)
G(.(x, nil)) → G(x)
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(.(.(x, y), z)) → F(.(x, .(y, z)))
G(.(x, .(y, z))) → G(.(.(x, y), z))
F(.(nil, y)) → F(y)
G(.(x, nil)) → G(x)
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G(.(x, .(y, z))) → G(.(.(x, y), z))
G(.(x, nil)) → G(x)
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(.(x, nil)) → G(x)
Used ordering: Polynomial interpretation [25,35]:
G(.(x, .(y, z))) → G(.(.(x, y), z))
The value of delta used in the strict ordering is 1/16.
POL(G(x1)) = (1/4)x_1
POL(.(x1, x2)) = x_1 + x_2
POL(nil) = 1/4
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
G(.(x, .(y, z))) → G(.(.(x, y), z))
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G(.(x, .(y, z))) → G(.(.(x, y), z))
The value of delta used in the strict ordering is 4.
POL(G(x1)) = (2)x_1
POL(.(x1, x2)) = 1/2 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
F(.(.(x, y), z)) → F(.(x, .(y, z)))
F(.(nil, y)) → F(y)
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(.(.(x, y), z)) → F(.(x, .(y, z)))
F(.(nil, y)) → F(y)
The value of delta used in the strict ordering is 1/16.
POL(.(x1, x2)) = 1/4 + (4)x_1 + x_2
POL(nil) = 0
POL(F(x1)) = (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))